Nuprl Lemma : exists_det_fun_a
13,42
postcript
pdf
T
:Type,
A
:(
T
). (
f
:detach_fun(
T
;
A
). True)
{
x
:
T
. Dec(
(
A
(
x
)))}
latex
Up
gen
algebra
1
Definitions
{
T
}
Lemmas
exists
det
fun
origin
T:Type, A:(T
). (
f:detach_fun(T;A). True) 
{x:T. Dec(
(A(x)))} T:Type, A:(T). (f:detach_fun(T;A). True) {x:T. Dec((A(x)))}